nLab Floris van Doorn

• webpage

Selected writings

On higher inductive types and (Atiyah-Hirzebruch-/Serre-)spectral sequences in homotopy type theory formalized in Lean (cf. cohomology in homotopy type theory and spectral sequences in homotopy type theory):

• Floris van Doorn, Spectral (github.com/cmu-phil/Spectral)

• Floris van Doorn, On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory (2018) [arXiv:1808.10690]

On $\infty$-groups formalized in homotopy type theory:

• Ulrik Buchholtz, Floris van Doorn, Egbert Rijke, Higher Groups in Homotopy Type Theory, LICS ‘18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (2018) 205-214 [arXiv:1802.04315, doi:10.1145/3209108.3209150]

Related entries

• Lean

• spectral sequence, Serre spectral sequence

category: people